Definitions | t T, L1 L2, P  Q, x:A. B(x), P & Q, P   Q, P  Q, Y, ||as||, False, A B, i j , x:A. B(x), A, T, ff, tt, if b then t else f fi , True, t ...$L, , increasing(f;k), i j < k, {i..j }, {T}, SQType(T), suptype(S; T), S T, , i <z j,  b, i z j, nth_tl(n;as), hd(l), l[i], no_repeats(T;l), Unit, , P Q, Dec(P),  |